-- Mathlib/MeasureTheory/Integral/Gamma.lean
theorem Complex.integral_rpow_mul_exp_neg_mul_rpow {p q b : ℝ} (hp : 1 ≤ p) (hq : - 2 < q)
    (hb : 0 < b) :
    ∫ x : ℂ, ‖x‖ ^ q * rexp (- b * ‖x‖ ^ p) = (2 * π / p) *
      b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p)

Proof state:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ ∫ (x : ℂ), ‖x‖ ^ q * rexp (-b * ‖x‖ ^ p) = 2 * π / p * b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p)

Tactic:
calc
  _ = ∫ x in Ioi (0 : ℝ) ×ˢ Ioo (-π) π, x.1 * (|x.1| ^ q * rexp (- b * |x.1| ^ p)) := by
    rw [← Complex.integral_comp_polarCoord_symm, polarCoord_target]
    simp_rw [Complex.norm_polarCoord_symm, smul_eq_mul]
  _ = (∫ x in Ioi (0 : ℝ), x * |x| ^ q * rexp (- b * |x| ^ p)) * ∫ _ in Ioo (-π) π, 1 := by
    rw [← setIntegral_prod_mul, volume_eq_prod]
    simp_rw [mul_one]
    congr! 2; ring
  _ = 2 * π * ∫ x in Ioi (0 : ℝ), x * |x| ^ q * rexp (- b * |x| ^ p) := by
    simp_rw [integral_const, Measure.restrict_apply MeasurableSet.univ, Set.univ_inter,
      volume_Ioo, sub_neg_eq_add, ← two_mul, ENNReal.toReal_ofReal (by positivity : 0 ≤ 2 * π),
      smul_eq_mul, mul_one, mul_comm]
  _ = 2 * π * ∫ x in Ioi (0 : ℝ), x ^ (q + 1) * rexp (-b * x ^ p) := by
    congr 1
    refine setIntegral_congr_fun measurableSet_Ioi (fun x hx => ?_)
    rw [mem_Ioi] at hx
    rw [abs_eq_self.mpr hx.le, rpow_add hx, rpow_one]
    ring
  _ = (2 * π / p) * b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p) := by
    rw [_root_.integral_rpow_mul_exp_neg_mul_rpow (by linarith) (by linarith) hb, add_assoc,
      one_add_one_eq_two]
    ring

Result:
no goals

Proof state:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ ∫ (p_1 : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π,
      p_1.1 • (‖↑Complex.polarCoord.symm p_1‖ ^ q * rexp (-b * ‖↑Complex.polarCoord.symm p_1‖ ^ p)) =
    ∫ (x : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, x.1 * (|x.1| ^ q * rexp (-b * |x.1| ^ p))

Tactic:
simp_rw [Complex.norm_polarCoord_symm, smul_eq_mul]

Result:
no goals

Proof state:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ -1 < q + 1

Tactic:
linarith

Result:
no goals

Proof state:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ (∫ (x : ℝ) in Ioi 0, x * |x| ^ q * rexp (-b * |x| ^ p)) * ∫ (x : ℝ) in Ioo (-π) π, 1 =
    2 * π * ∫ (x : ℝ) in Ioi 0, x * |x| ^ q * rexp (-b * |x| ^ p)

Tactic:
simp_rw [integral_const, Measure.restrict_apply MeasurableSet.univ, Set.univ_inter,
  volume_Ioo, sub_neg_eq_add, ← two_mul, ENNReal.toReal_ofReal (by positivity : 0 ≤ 2 * π),
  smul_eq_mul, mul_one, mul_comm]

Result:
no goals

Proof state:
case e_a
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
x : ℝ
hx : x ∈ Ioi 0
⊢ x * |x| ^ q * rexp (-b * |x| ^ p) = x ^ (q + 1) * rexp (-b * x ^ p)

Tactic:
rw [mem_Ioi] at hx

Result:
case e_a
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
x : ℝ
hx : 0 < x
⊢ x * |x| ^ q * rexp (-b * |x| ^ p) = x ^ (q + 1) * rexp (-b * x ^ p)

Proof state:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ ∫ (x : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, x.1 * (|x.1| ^ q * rexp (-b * |x.1| ^ p)) ∂volume.prod volume =
    ∫ (z : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, z.1 * |z.1| ^ q * rexp (-b * |z.1| ^ p) * 1 ∂volume.prod volume

Tactic:
simp_rw [mul_one]

Result:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ ∫ (x : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, x.1 * (|x.1| ^ q * rexp (-b * |x.1| ^ p)) ∂volume.prod volume =
    ∫ (z : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, z.1 * |z.1| ^ q * rexp (-b * |z.1| ^ p) ∂volume.prod volume

Proof state:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ 2 * π * (b ^ (-(q + 2) / p) * (1 / p) * Real.Gamma ((q + 2) / p)) =
    2 * π / p * b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p)

Tactic:
ring

Result:
no goals

Proof state:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ 2 * π * ∫ (x : ℝ) in Ioi 0, x ^ (q + 1) * rexp (-b * x ^ p) =
    2 * π / p * b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p)

Tactic:
rw [_root_.integral_rpow_mul_exp_neg_mul_rpow (by linarith) (by linarith) hb, add_assoc,
  one_add_one_eq_two]

Result:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ 2 * π * (b ^ (-(q + 2) / p) * (1 / p) * Real.Gamma ((q + 2) / p)) =
    2 * π / p * b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p)

Proof state:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ ∫ (x : ℂ), ‖x‖ ^ q * rexp (-b * ‖x‖ ^ p) =
    ∫ (x : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, x.1 * (|x.1| ^ q * rexp (-b * |x.1| ^ p))

Tactic:
rw [← Complex.integral_comp_polarCoord_symm, polarCoord_target]

Result:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ ∫ (p_1 : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π,
      p_1.1 • (‖↑Complex.polarCoord.symm p_1‖ ^ q * rexp (-b * ‖↑Complex.polarCoord.symm p_1‖ ^ p)) =
    ∫ (x : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, x.1 * (|x.1| ^ q * rexp (-b * |x.1| ^ p))

Proof state:
case h.e'_7.h
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
x✝ : ℝ × ℝ
⊢ x✝.1 * (|x✝.1| ^ q * rexp (-b * |x✝.1| ^ p)) = x✝.1 * |x✝.1| ^ q * rexp (-b * |x✝.1| ^ p)

Tactic:
ring

Result:
no goals

Proof state:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ ∫ (x : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, x.1 * (|x.1| ^ q * rexp (-b * |x.1| ^ p)) ∂volume.prod volume =
    ∫ (z : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, z.1 * |z.1| ^ q * rexp (-b * |z.1| ^ p) ∂volume.prod volume

Tactic:
congr! 2

Result:
case h.e'_7.h
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
x✝ : ℝ × ℝ
⊢ x✝.1 * (|x✝.1| ^ q * rexp (-b * |x✝.1| ^ p)) = x✝.1 * |x✝.1| ^ q * rexp (-b * |x✝.1| ^ p)

Proof state:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ 2 * π * ∫ (x : ℝ) in Ioi 0, x * |x| ^ q * rexp (-b * |x| ^ p) =
    2 * π * ∫ (x : ℝ) in Ioi 0, x ^ (q + 1) * rexp (-b * x ^ p)

Tactic:
congr 1

Result:
case e_a
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ ∫ (x : ℝ) in Ioi 0, x * |x| ^ q * rexp (-b * |x| ^ p) = ∫ (x : ℝ) in Ioi 0, x ^ (q + 1) * rexp (-b * x ^ p)

Proof state:
case e_a
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
x : ℝ
hx : 0 < x
⊢ x * x ^ q * rexp (-b * x ^ p) = x ^ q * x * rexp (-b * x ^ p)

Tactic:
ring

Result:
no goals

Proof state:
case e_a
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ ∫ (x : ℝ) in Ioi 0, x * |x| ^ q * rexp (-b * |x| ^ p) = ∫ (x : ℝ) in Ioi 0, x ^ (q + 1) * rexp (-b * x ^ p)

Tactic:
refine setIntegral_congr_fun measurableSet_Ioi (fun x hx => ?_)

Result:
case e_a
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
x : ℝ
hx : x ∈ Ioi 0
⊢ x * |x| ^ q * rexp (-b * |x| ^ p) = x ^ (q + 1) * rexp (-b * x ^ p)

Proof state:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ ∫ (x : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, x.1 * (|x.1| ^ q * rexp (-b * |x.1| ^ p)) =
    (∫ (x : ℝ) in Ioi 0, x * |x| ^ q * rexp (-b * |x| ^ p)) * ∫ (x : ℝ) in Ioo (-π) π, 1

Tactic:
rw [← setIntegral_prod_mul, volume_eq_prod]

Result:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ ∫ (x : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, x.1 * (|x.1| ^ q * rexp (-b * |x.1| ^ p)) ∂volume.prod volume =
    ∫ (z : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, z.1 * |z.1| ^ q * rexp (-b * |z.1| ^ p) * 1 ∂volume.prod volume

Proof state:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ 0 ≤ 2 * π

Tactic:
positivity

Result:
no goals

Proof state:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ 0 < p

Tactic:
linarith

Result:
no goals

Proof state:
case e_a
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
x : ℝ
hx : 0 < x
⊢ x * |x| ^ q * rexp (-b * |x| ^ p) = x ^ (q + 1) * rexp (-b * x ^ p)

Tactic:
rw [abs_eq_self.mpr hx.le, rpow_add hx, rpow_one]

Result:
case e_a
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
x : ℝ
hx : 0 < x
⊢ x * x ^ q * rexp (-b * x ^ p) = x ^ q * x * rexp (-b * x ^ p)