English
There exists a measure μ on R such that for every nonnegative a, the integral representation holds: a^p equals the product of μ-related integrals, with integrability on Ioi 0.
Русский
Существет мера μ на R так, что для любого неотрицательного a выполняется интегральное представление: a^p выражается через интегралы, при этом интегрируемость на Ioi 0 соблюдается.
LaTeX
$$$\\exists \\mu:\\,\\mathrm{Measure}\\,\\mathbb{R},\\;\\forall a\\ge 0:\\; (\\mathrm{IntegrableOn}\\, (p\\rpowIntegrand_{01} t\\, a)\\, (Ioi 0)\\, \\mu) \\land a^{p} = \\int_{0}^{\\infty} p\\rpowIntegrand_{01} t\\, a\\; d\\mu$$$
Lean4
/-- The integral representation of the function `x ↦ x ^ p` (where `p ∈ (0, 1)`) . -/
theorem exists_measure_rpow_eq_integral (hp : p ∈ Ioo 0 1) :
∃ μ : Measure ℝ,
∀ x ∈ Ici 0,
(IntegrableOn (fun t => rpowIntegrand₀₁ p t x) (Ioi 0) μ) ∧ x ^ p = ∫ t in Ioi 0, rpowIntegrand₀₁ p t x ∂μ :=
by
let C : ℝ≥0 :=
{ val := (∫ t in Ioi 0, rpowIntegrand₀₁ p t 1)⁻¹
property := by
rw [inv_nonneg]
exact le_of_lt <| integral_rpowIntegrand₀₁_one_pos hp }
refine ⟨C • volume, fun x hx => ⟨?_, ?_⟩⟩
· unfold IntegrableOn
rw [Measure.restrict_smul]
exact Integrable.smul_measure_nnreal <| integrableOn_rpowIntegrand₀₁_Ioi hp hx
·
simp_rw [Measure.restrict_smul, integral_smul_nnreal_measure, rpow_eq_const_mul_integral hp hx, NNReal.smul_def, C,
NNReal.coe_mk, smul_eq_mul]
