-- Mathlib/Analysis/MellinTransform.lean
theorem mellin_comp_rpow (f : ℝ → E) (s : ℂ) (a : ℝ) :
    mellin (fun t => f (t ^ a)) s = |a|⁻¹ • mellin f (s / a)

Proof state:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (s - 1) • f (t ^ a) = (↑(t ^ (a - 1)) * ↑(t ^ a) ^ (s / ↑a - 1)) • f (t ^ a)

Tactic:
rw [ofReal_cpow (le_of_lt ht), ← cpow_mul_ofReal_nonneg (le_of_lt ht), ←
  cpow_add _ _ (ofReal_ne_zero.mpr <| ne_of_gt ht), ofReal_sub, ofReal_one, mul_sub,
  mul_div_cancel₀ _ (ofReal_ne_zero.mpr ha), add_comm, ← add_sub_assoc, mul_one, sub_add_cancel]

Result:
no goals

Proof state:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
hE : CompleteSpace E
⊢ mellin (fun t => f (t ^ 0)) s = |0|⁻¹ • mellin f (s / ↑0)

Tactic:
simp [integral_smul_const, mellin, setIntegral_Ioi_zero_cpow]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
⊢ mellin (fun t => f (t ^ a)) s = |a|⁻¹ • mellin f (s / ↑a)

Tactic:
rcases eq_or_ne a 0 with rfl|ha

Result:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
⊢ mellin (fun t => f (t ^ 0)) s = |0|⁻¹ • mellin f (s / ↑0)

case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
⊢ mellin (fun t => f (t ^ a)) s = |a|⁻¹ • mellin f (s / ↑a)

Proof state:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
⊢ mellin (fun t => f (t ^ 0)) s = |0|⁻¹ • mellin f (s / ↑0)

Tactic:
by_cases hE : CompleteSpace E

Result:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
hE : CompleteSpace E
⊢ mellin (fun t => f (t ^ 0)) s = |0|⁻¹ • mellin f (s / ↑0)

case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
hE : ¬CompleteSpace E
⊢ mellin (fun t => f (t ^ 0)) s = |0|⁻¹ • mellin f (s / ↑0)

Proof state:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
⊢ ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • f (t ^ a) = |a|⁻¹ • ∫ (t : ℝ) in Ioi 0, ↑t ^ (s / ↑a - 1) • f t

Tactic:
conv_rhs => rw [← integral_comp_rpow_Ioi _ ha, ← integral_smul]

Result:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
⊢ ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • f (t ^ a) =
    ∫ (a_1 : ℝ) in Ioi 0, |a|⁻¹ • (|a| * a_1 ^ (a - 1)) • ↑(a_1 ^ a) ^ (s / ↑a - 1) • f (a_1 ^ a)

Proof state:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (s - 1) • f (t ^ a) = |a|⁻¹ • (|a| * t ^ (a - 1)) • ↑(t ^ a) ^ (s / ↑a - 1) • f (t ^ a)

Tactic:
rw [← mul_smul, ← mul_assoc, inv_mul_cancel₀ (mt abs_eq_zero.1 ha), one_mul, ← smul_assoc,
  real_smul]

Result:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (s - 1) • f (t ^ a) = (↑(t ^ (a - 1)) * ↑(t ^ a) ^ (s / ↑a - 1)) • f (t ^ a)

Proof state:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
⊢ mellin (fun t => f (t ^ a)) s = |a|⁻¹ • mellin f (s / ↑a)

Tactic:
simp_rw [mellin]

Result:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
⊢ ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • f (t ^ a) = |a|⁻¹ • ∫ (t : ℝ) in Ioi 0, ↑t ^ (s / ↑a - 1) • f t

Proof state:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
⊢ ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • f (t ^ a) =
    ∫ (a_1 : ℝ) in Ioi 0, |a|⁻¹ • (|a| * a_1 ^ (a - 1)) • ↑(a_1 ^ a) ^ (s / ↑a - 1) • f (a_1 ^ a)

Tactic:
refine setIntegral_congr_fun measurableSet_Ioi fun t ht => ?_

Result:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (s - 1) • f (t ^ a) = |a|⁻¹ • (|a| * t ^ (a - 1)) • ↑(t ^ a) ^ (s / ↑a - 1) • f (t ^ a)

Proof state:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
hE : ¬CompleteSpace E
⊢ mellin (fun t => f (t ^ 0)) s = |0|⁻¹ • mellin f (s / ↑0)

Tactic:
simp [integral, mellin, hE]

Result:
no goals