English
For hp ∈ (0,1) and x ≥ 0, x^p equals the quotient of the two integrals: integral_rpowIntegrand₀₁_eq_rpow_mul_integral expresses x^p as a product with the integral of rpowIntegrand₀₁ p t x.
Русский
Для p ∈ (0,1) и x ≥ 0 x^p выражается через интеграл rpowIntegrand₀₁ и константу, связав две части интегрального выражения.
LaTeX
$$$x^{p} = \\biggl(\\int_{0}^{\\infty} rpowIntegrand_{01} p\\, t\\, 1\\, dt\\biggr)^{-1} \\; \\int_{0}^{\\infty} rpowIntegrand_{01} p\\, t\\, x\\, dt$$$
Lean4
/-- The integral representation of the function `x ↦ x^p` (where `p ∈ (0, 1)`) . -/
theorem rpow_eq_const_mul_integral (hp : p ∈ Ioo 0 1) (hx : 0 ≤ x) :
x ^ p = (∫ t in Ioi 0, rpowIntegrand₀₁ p t 1)⁻¹ * ∫ t in Ioi 0, rpowIntegrand₀₁ p t x :=
by
rcases eq_or_lt_of_le' hx with hx_zero | _
case inl =>
simp only [mem_Ioo] at hp
simp [hx_zero, Real.zero_rpow (by linarith)]
case inr =>
have : ∫ t in Ioi 0, rpowIntegrand₀₁ p t 1 ≠ 0 := ne_of_gt <| integral_rpowIntegrand₀₁_one_pos hp
rw [integral_rpowIntegrand₀₁_eq_rpow_mul_const hp hx, mul_comm, mul_assoc, mul_inv_cancel₀ this, mul_one]
