-- Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean
theorem functional_equation (s : ℂ) :
    P.Λ (P.k - s) = P.ε • P.symm.Λ s

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s
⊢ mellin P.f (↑P.k - s) = P.ε • mellin P.g s

Tactic:
have step2 := mellin_cpow_smul (fun t ↦ P.g (1 / t)) (P.k - s) (-P.k)

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin (fun t => P.g (1 / t)) (↑P.k - s + -↑P.k)
⊢ mellin P.f (↑P.k - s) = P.ε • mellin P.g s

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s
step3 :
  mellin (fun t => P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) =
    P.ε • mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s)
⊢ mellin P.f (↑P.k - s) = P.ε • mellin P.g s

Tactic:
rw [step2] at step3

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s
step3 : mellin (fun t => P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = P.ε • mellin P.g s
⊢ mellin P.f (↑P.k - s) = P.ε • mellin P.g s

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s
⊢ mellin P.f (↑P.k - s) = P.ε • mellin P.g s

Tactic:
have step3 := mellin_const_smul (fun t ↦ (t : ℂ) ^ (-P.k : ℂ) • P.g (1 / t)) (P.k - s) P.ε

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s
step3 :
  mellin (fun t => P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) =
    P.ε • mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s)
⊢ mellin P.f (↑P.k - s) = P.ε • mellin P.g s

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s
step3 : mellin (fun t => P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = P.ε • mellin P.g s
⊢ mellin P.f (↑P.k - s) = mellin (fun t => P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s)

Tactic:
refine setIntegral_congr_fun measurableSet_Ioi (fun t ht ↦ ?_)

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s
step3 : mellin (fun t => P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = P.ε • mellin P.g s
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (↑P.k - s - 1) • P.f t = ↑t ^ (↑P.k - s - 1) • (fun t => P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) t

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s
step3 : mellin (fun t => P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = P.ε • mellin P.g s
t : ℝ
ht : t ∈ Ioi 0
this : ↑t ^ ↑P.k ≠ 0
⊢ ↑t ^ (↑P.k - s - 1) • P.f t = (↑t ^ (↑P.k - s - 1) * (P.ε * ((↑t ^ ↑P.k)⁻¹ * (P.ε⁻¹ * ↑t ^ ↑P.k)))) • P.f t

Tactic:
field_simp [P.hε]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
⊢ mellin P.f (↑P.k - s) = P.ε • mellin P.g s

Tactic:
have step1 := mellin_comp_rpow P.g (-s) (-1)

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun t => P.g (t ^ (-1))) (-s) = |(-1)|⁻¹ • mellin P.g (-s / ↑(-1))
⊢ mellin P.f (↑P.k - s) = P.ε • mellin P.g s

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s
step3 : mellin (fun t => P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = P.ε • mellin P.g s
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (↑P.k - s - 1) • P.f t = (↑t ^ (↑P.k - s - 1) * (P.ε * (↑t ^ (-↑P.k) * (P.ε⁻¹ * ↑(t ^ P.k))))) • P.f t

Tactic:
rw [cpow_neg, ofReal_cpow (le_of_lt ht)]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s
step3 : mellin (fun t => P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = P.ε • mellin P.g s
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (↑P.k - s - 1) • P.f t = (↑t ^ (↑P.k - s - 1) * (P.ε * ((↑t ^ ↑P.k)⁻¹ * (P.ε⁻¹ * ↑t ^ ↑P.k)))) • P.f t

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s
step3 : mellin (fun t => P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = P.ε • mellin P.g s
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (↑P.k - s - 1) • P.f t = (↑t ^ (↑P.k - s - 1) * (P.ε * ((↑t ^ ↑P.k)⁻¹ * (P.ε⁻¹ * ↑t ^ ↑P.k)))) • P.f t

Tactic:
have : (t : ℂ) ^ (P.k : ℂ) ≠ 0 := by simpa [← ofReal_cpow ht.le] using (rpow_pos_of_pos ht _).ne'

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s
step3 : mellin (fun t => P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = P.ε • mellin P.g s
t : ℝ
ht : t ∈ Ioi 0
this : ↑t ^ ↑P.k ≠ 0
⊢ ↑t ^ (↑P.k - s - 1) • P.f t = (↑t ^ (↑P.k - s - 1) * (P.ε * ((↑t ^ ↑P.k)⁻¹ * (P.ε⁻¹ * ↑t ^ ↑P.k)))) • P.f t

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin (fun t => P.g (1 / t)) (↑P.k - s + -↑P.k)
⊢ mellin P.f (↑P.k - s) = P.ε • mellin P.g s

Tactic:
rw [← sub_eq_add_neg, sub_right_comm, sub_self, zero_sub, step1] at step2

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s
⊢ mellin P.f (↑P.k - s) = P.ε • mellin P.g s

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
⊢ P.Λ (↑P.k - s) = P.ε • P.symm.Λ s

Tactic:
rw [P.Λ_eq, P.symm_Λ_eq]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
⊢ mellin P.f (↑P.k - s) = P.ε • mellin P.g s

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s
step3 : mellin (fun t => P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = P.ε • mellin P.g s
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ ↑P.k ≠ 0

Tactic:
simpa [← ofReal_cpow ht.le] using (rpow_pos_of_pos ht _).ne'

Result:
no goals