English
The core functional equation for a strong FE pair states that Λ evaluated at k − s equals ε times the symmetric Λ at s; i.e., Λ(k − s) = ε · symm.Λ(s).
Русский
Ключевое функциональное уравнение сильной FE-пары: Λ(k − s) = ε · симм.Λ(s).
LaTeX
$$functional_equation (s : Complex) : Λ(k − s) = ε · symm.Λ(s)$$
Lean4
/-- Main theorem about strong FE pairs: if `(f, g)` are a strong FE pair, then the Mellin
transforms of `f` and `g` are related by `s ↦ k - s`.
This is proved by making a substitution `t ↦ t⁻¹` in the Mellin transform integral. -/
theorem functional_equation (s : ℂ) : P.Λ (P.k - s) = P.ε • P.symm.Λ s := by
-- unfold definition:
rw [P.Λ_eq, P.symm_Λ_eq]
-- substitute `t ↦ t⁻¹` in `mellin P.g s`
have step1 := mellin_comp_rpow P.g (-s) (-1)
simp_rw [abs_neg, abs_one, inv_one, one_smul, ofReal_neg, ofReal_one, div_neg, div_one, neg_neg, rpow_neg_one, ←
one_div] at step1
have step2 := mellin_cpow_smul (fun t ↦ P.g (1 / t)) (P.k - s) (-P.k)
rw [← sub_eq_add_neg, sub_right_comm, sub_self, zero_sub, step1] at step2
have step3 := mellin_const_smul (fun t ↦ (t : ℂ) ^ (-P.k : ℂ) • P.g (1 / t)) (P.k - s) P.ε
rw [step2] at step3
rw [← step3]
-- now the integrand matches `P.h_feq'` on `Ioi 0`, so we can apply `setIntegral_congr_fun`
refine setIntegral_congr_fun measurableSet_Ioi (fun t ht ↦ ?_)
simp_rw [P.h_feq' t ht, ← mul_smul]
-- some simple `cpow` arithmetic to finish
rw [cpow_neg, ofReal_cpow (le_of_lt ht)]
have : (t : ℂ) ^ (P.k : ℂ) ≠ 0 := by simpa [← ofReal_cpow ht.le] using (rpow_pos_of_pos ht _).ne'
field_simp [P.hε]
