English
The integrand with argument x·t relates to the product of the integrand at t with 1 scaled by x: rpowIntegrand(p, x·t, x) = (rpowIntegrand(p, t, 1)) · x^(p-1).
Русский
Интегранг с аргументом x·t связан с произведением интегранга при t на 1, масштабированного x: rpowIntegrand(p, x·t, x) = rpowIntegrand(p, t, 1) · x^(p-1).
LaTeX
$$$\mathrm{rpowIntegrand}_{01}(p, x\cdot t, x) = \mathrm{rpowIntegrand}_{01}(p,t,1) \cdot x^{\,p-1}$$$
Lean4
theorem rpowIntegrand₀₁_apply_mul (hp : p ∈ Ioo 0 1) (ht : 0 ≤ t) (hx : 0 ≤ x) :
rpowIntegrand₀₁ p (x * t) x = (rpowIntegrand₀₁ p t 1) * x ^ (p - 1) :=
by
have hxt : 0 ≤ x * t := by positivity
rw [rpowIntegrand₀₁_eq_pow_div hp hxt hx, rpowIntegrand₀₁_eq_pow_div hp ht zero_le_one]
by_cases hx_zero : x = 0
case neg =>
calc
_ = x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x))) := by rw [← mul_assoc, mul_div_assoc, Real.mul_rpow hx ht]
_ = x ^ (p - 1) * (t ^ (p - 1) * 1 / (t + 1)) :=
by
have : x * t + x = x * (t + 1) := by ring
rw [mul_div_assoc, this, div_mul_eq_div_mul_one_div, div_self hx_zero, one_mul]
_ = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1) := by rw [mul_comm]
case pos =>
rw [mem_Ioo] at hp
simp [hx_zero, Real.zero_rpow (by linarith : p - 1 ≠ 0)]
