RealAxisMellinPole.lean

1 import PaperX.RealAxisMellinMoment
2 import PaperX.RealAxisPoleRigidity
3 
4 /-! Assembly of the real-axis integral and pole arguments. The required
5 arithmetic product identity and summatory-function bounds remain hypotheses. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.RealAxisMellinPole
9 open Filter Asymptotics MeasureTheory Set
10 open scoped Topology
11 
12 /-- The real and complex casts of the real endpoint parameter have the same norm. -/
13 theorem isBigO_complex_scale_iff {f : ℝ → ℂ} {l : Filter ℝ} :
14     f =O[l] (fun h : ℝ => (h : ℂ)) ↔ f =O[l] (fun h : ℝ => h) := by
15   simp only [Asymptotics.isBigO_iff, Complex.norm_real]
16 
17 /-- Power-saving bounds on the supplied summatory functions suffice for the
18 pole-product conclusion without complex analytic continuation. -/
19 theorem index_one_and_mellin_values_nonzero {ι : Type*} [Fintype ι]
20     (S : ι → ℝ → ℂ) (C r : ι → ℝ) (p Z : ℝ → ℂ) (P Q : ℂ) (d : ℕ)
21     (hS : ∀ i, AEStronglyMeasurable (S i) (volume.restrict (Ioi 1)))
22     (hr : ∀ i, r i < 1)
23     (hbound : ∀ i x, 1 < x → ‖S i x‖ ≤ C i * x ^ r i)
24     (hp : Tendsto (fun h : ℝ => (h : ℂ) * p h) (𝓝[>] 0) (𝓝 P)) (hP : P ≠ 0)
25     (hZ : Tendsto (fun h : ℝ => (h : ℂ) * Z h) (𝓝[>] 0) (𝓝 Q)) (hQ : Q ≠ 0)
26     (hid : Z =ᶠ[𝓝[>] 0] fun h =>
27       (p h * ∏ i, RealAxisMellinMoment.mellinIntegral (S i) h) ^ d) :
28     d = 1 ∧ ∀ i, RealAxisMellinMoment.mellinIntegral (S i) 0 ≠ 0 := by
29   apply RealAxisPoleRigidity.right_endpoint_index_one_and_factors_nonzero
30     p Z (fun i => RealAxisMellinMoment.mellinIntegral (S i)) P Q d hp hP hZ hQ _ hid
31   intro i
32   exact isBigO_complex_scale_iff.mpr
33     (RealAxisMellinMoment.mellinIntegral_sub_isBigO_of_power_bound (hS i) (hr i) (hbound i))
34 
35 end PaperX.RealAxisMellinPole

Back to source controls