integrable_exp_neg_mul_sq
theorem integrable_exp_neg_mul_sq :
∀ {b : ℝ}, 0 < b → MeasureTheory.Integrable (fun x => (-b * x ^ 2).exp) MeasureTheory.volume
The theorem `integrable_exp_neg_mul_sq` states that for any positive real number `b`, the function `x => Real.exp (-b * x ^ 2)`, which represents the real exponential of the negative product of `b` and the square of `x`, is integrable with respect to the Lebesgue measure. In other words, this function is measurable and the integral over its entire domain of the norm of its value at each point is finite. This integral corresponds to the total "signed area" under the graph of the function.
More concisely: The function `x => Real.exp (-b * x ^ 2)` is integrable with respect to the Lebesgue measure for any positive real number `b`.
|
norm_cexp_neg_mul_sq
theorem norm_cexp_neg_mul_sq : ∀ (b : ℂ) (x : ℝ), ‖(-b * ↑x ^ 2).exp‖ = (-b.re * x ^ 2).exp
This theorem states that for any complex number `b` and any real number `x`, the norm of the complex exponential function applied to the product of `-b` and the square of `x` is equal to the real exponential function applied to the product of the negative of the real part of `b` and the square of `x`. In mathematical terms, for all complex `b` and real `x`, we have ||exp(-b * x^2)|| = exp(-Re(b) * x^2).
More concisely: For all complex numbers `b` and real numbers `x`, ||exp(-b * x^2)|| = exp(-Re(b) * x^2).
Alternatively, the norm of the complex exponential function of `-b * x^2` equals the real exponential function of `-Re(b) * x^2`.
|
Real.Gamma_one_half_eq
theorem Real.Gamma_one_half_eq : (1 / 2).Gamma = Real.pi.sqrt
This theorem states that the gamma function evaluated at one-half is equal to the square root of pi. In mathematical terms, it is commonly written as `Γ(1/2) = √π`. This is a special value formula equivalent to the Gaussian integral, which is a key result in probability theory and quantum mechanics.
More concisely: The gamma function equals the square root of pi at the input of one-half: `Γ(1/2) = √π`.
|
integral_gaussian_sq_complex
theorem integral_gaussian_sq_complex : ∀ {b : ℂ}, 0 < b.re → (∫ (x : ℝ), (-b * ↑x ^ 2).exp) ^ 2 = ↑Real.pi / b := by
sorry
This theorem states that for any complex number `b` with a positive real part, the square of the Gaussian integral, which is the integral over all real numbers `x` of `exp (-b * x^2)`, is equal to the real number π divided by `b`. In mathematical notation, it asserts that for all `b` in the complex numbers with a positive real part, the square of the integral from negative infinity to infinity of `exp(-b * x^2) dx` is equal to `π / b`.
More concisely: For any complex number `b` with a positive real part, the square of the Gaussian integral over all real numbers `x` of `exp(-b * x^2) dx` equals `π / b`.
|
Complex.Gamma_one_half_eq
theorem Complex.Gamma_one_half_eq : (1 / 2).Gamma = ↑Real.pi ^ (1 / 2)
This theorem is about a special-value formula in complex analysis. It states that the Gamma function at 1/2 is equal to the square root of the number pi (π). In mathematical terms, it's written as Γ(1/2) = √π. This formula is equivalent to the Gaussian integral, a well-known result in probability theory and statistics.
More concisely: The Gamma function evaluates to the square root of pi at the argument 1/2: Γ(1/2) = √π.
|