English
Let p ∈ (0,1) and x ≥ 0. The integral of rpowIntegrand with argument x scales as x^p times the integral with x = 1.
Русский
Пусть p ∈ (0,1) и x ≥ 0. Интеграл rpowIntegrand p t x по t равно x^p умножить на интеграл rpowIntegrand p t 1.
LaTeX
$$$p \in (0,1),\; x \ge 0:\; \int_{0}^{\infty} rpowIntegrand_{01}(p,t,x) \, dt = x^{p} \int_{0}^{\infty} rpowIntegrand_{01}(p,t,1) \, dt$$$
Lean4
theorem integral_rpowIntegrand₀₁_eq_rpow_mul_const (hp : p ∈ Ioo 0 1) (hx : 0 ≤ x) :
(∫ t in Ioi 0, rpowIntegrand₀₁ p t x) = x ^ p * (∫ t in Ioi 0, rpowIntegrand₀₁ p t 1) := by
-- We use the change of variables formula with `f t = x * t`. Here `g = rpowIntegrand₀₁ p · x`.
obtain (rfl | hx) := hx.eq_or_lt
· simp [rpowIntegrand₀₁, Real.zero_rpow hp.1.ne']
suffices ∫ t in Ioi 0, ((rpowIntegrand₀₁ p · x) ∘ (x * ·)) t * x = x ^ p * (∫ t in Ioi 0, rpowIntegrand₀₁ p t 1)
by
rwa [integral_comp_mul_deriv_Ioi (by fun_prop), mul_zero] at this
· exact tendsto_id.const_mul_atTop hx
· simpa using fun t _ ↦ hasDerivWithinAt_id t (Ioi t) |>.const_mul x
· simpa [Set.image_mul_left_Ioi hx] using continuousOn_rpowIntegrand₀₁ hp hx.le
· simpa [Set.image_mul_left_Ici hx] using integrableOn_rpowIntegrand₀₁_Ici hp hx.le
· simp only [Function.comp]
rw [integrableOn_congr_fun (rpowIntegrand₀₁_apply_mul_eqOn_Ici hp hx.le) measurableSet_Ici]
exact Integrable.mul_const (integrableOn_rpowIntegrand₀₁_Ici hp zero_le_one) _
have heqOn : EqOn (fun t => rpowIntegrand₀₁ p (x * t) x * x) (fun t => (rpowIntegrand₀₁ p t 1) * x ^ p) (Ioi 0) :=
EqOn.mono Ioi_subset_Ici_self (rpowIntegrand₀₁_apply_mul_eqOn_Ici hp hx.le)
simp only [Function.comp, setIntegral_congr_fun measurableSet_Ioi heqOn, ← smul_eq_mul (b := x ^ p),
integral_smul_const]
rw [smul_eq_mul, mul_comm]
