rpowIntegrand₀₁_eqOn_mul_rpowIntegrand₀₁_one

English

For p ∈ (0,1) and t > 0 the equality (rpowIntegrand₀₁ p t) is equivalent to t^(p-1) times rpowIntegrand₀₁ p 1 (t⁻¹·x) on Ici 0.

Русский

Для p ∈ (0,1) и t > 0 равенство (rpowIntegrand₀₁ p t) эквивалентно t^(p-1)·rpowIntegrand₀₁ p 1 (t⁻¹·x) на множестве Ici 0.

LaTeX

$$$\\forall p,t>0:\\; (rpowIntegrand_{01} p\\, t) = t^{p-1}\\cdot rpowIntegrand_{01} p\\, 1\\left(t^{-1}\\cdot x\\right)\\quad\\text{on }(Ici\\,0)$$$

Lean4

theorem rpowIntegrand₀₁_eqOn_mul_rpowIntegrand₀₁_one (ht : 0 < t) :
    (Ici 0).EqOn (rpowIntegrand₀₁ p t) (fun x => t ^ (p - 1) * (rpowIntegrand₀₁ p 1 (t⁻¹ • x))) :=
  by
  intro x hx
  calc
    _ = t ^ p * (t⁻¹ - t⁻¹ * (1 + x * t⁻¹)⁻¹) := by simp [field, rpowIntegrand₀₁]
    _ = t ^ (p - 1) * (1 - (1 + x * t⁻¹)⁻¹) := by
      rw [Real.rpow_sub_one ht.ne']
      field_simp
    _ = _ := by
      simp [mul_comm, smul_eq_mul, rpowIntegrand₀₁]
        /- This lemma is private because it is strictly weaker than `integrableOn_rpowIntegrand₀₁_Ioi` -/

Похожие утверждения