RealAxisMellinMoment.lean

1 import PaperX.RealAxisEndpointIntegral
2 import Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
3 import Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
4 
5 /-! A power-saving bound on an actual measurable summatory function supplies the
6 logarithmic moment required by the real-axis endpoint theorem. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperX.RealAxisMellinMoment
10 open MeasureTheory Filter Set
11 open scoped Topology
12 
13 /-- A logarithmic weight costs any fixed positive power. -/
14 theorem weighted_power_bound {x r ε C : ℝ} {z : ℂ}
15     (hx : 1 < x) (hε : 0 < ε) (hz : ‖z‖ ≤ C * x ^ r) :
16     (1 + Real.log x) * ‖(x ^ (-2 : ℝ)) • z‖ ≤
17       (C * (1 + ε⁻¹)) * x ^ (r + ε - 2) := by
18   have hx0 : 0 < x := lt_trans zero_lt_one hx
19   have hxε : 1 ≤ x ^ ε := Real.one_le_rpow hx.le hε.le
20   have hl : Real.log x ≤ x ^ ε / ε := Real.log_le_rpow_div hx0.le hε
21   have hl0 : 0 ≤ Real.log x := Real.log_nonneg hx.le
22   have hweight : 1 + Real.log x ≤ (1 + ε⁻¹) * x ^ ε := by
23     calc
24       1 + Real.log x ≤ x ^ ε + x ^ ε / ε := add_le_add hxε hl
25       _ = (1 + ε⁻¹) * x ^ ε := by ring
26   rw [norm_smul, Real.norm_eq_abs, abs_of_pos (Real.rpow_pos_of_pos hx0 _)]
27   calc
28     (1 + Real.log x) * (x ^ (-2 : ℝ) * ‖z‖) ≤
29         ((1 + ε⁻¹) * x ^ ε) * (x ^ (-2 : ℝ) * (C * x ^ r)) := by
30       apply mul_le_mul hweight
31         (mul_le_mul_of_nonneg_left hz (Real.rpow_nonneg hx0.le _))
32         (mul_nonneg (Real.rpow_nonneg hx0.le _) (norm_nonneg z))
33       positivity
34     _ = (C * (1 + ε⁻¹)) * x ^ (r + ε - 2) := by
35       rw [show r + ε - 2 = ε + (-2 + r) by ring,
36         Real.rpow_add hx0, Real.rpow_add hx0]
37       ring
38 
39 /-- Any exponent strictly below one gives the needed logarithmic first moment. -/
40 theorem integrable_weighted_moment_of_power_bound {S : ℝ → ℂ} {C r : ℝ}
41     (hS : AEStronglyMeasurable S (volume.restrict (Ioi 1)))
42     (hr : r < 1)
43     (hbound : ∀ x, 1 < x → ‖S x‖ ≤ C * x ^ r) :
44     Integrable (fun x : ℝ => (1 + Real.log x) * ‖(x ^ (-2 : ℝ)) • S x‖)
45       (volume.restrict (Ioi 1)) := by
46   let ε : ℝ := (1 - r) / 2
47   have hε : 0 < ε := by dsimp [ε]; linarith
48   have hexp : r + ε - 2 < -1 := by dsimp [ε]; linarith
49   have hpow := integrableOn_Ioi_rpow_of_lt hexp (show (0 : ℝ) < 1 by norm_num)
50   apply (hpow.const_mul (C * (1 + ε⁻¹))).mono'
51   · have hm : Measurable (fun x : ℝ => x ^ (-2 : ℝ)) := by fun_prop
52     have hl : Measurable (fun x : ℝ => 1 + Real.log x) := by fun_prop
53     exact hl.aestronglyMeasurable.mul ((hm.aestronglyMeasurable.smul hS).norm)
54   · filter_upwards [ae_restrict_mem measurableSet_Ioi] with x hx
55     have hx1 : 1 < x := hx
56     have hl0 : 0 ≤ Real.log x := Real.log_nonneg hx1.le
57     rw [Real.norm_eq_abs, abs_of_nonneg (by positivity)]
58     exact weighted_power_bound hx1 hε (hbound x hx1)
59 
60 /-- The Mellin integral in the real parameter h=s-1. -/
61 def mellinIntegral (S : ℝ → ℂ) (h : ℝ) : ℂ :=
62   (1 + h) • ∫ x in Ioi (1 : ℝ), (x ^ (-2 - h)) • S x
63 
64 /-- The Mellin kernel is exactly the exponential damping kernel. -/
65 theorem mellinIntegral_eq_endpointIntegral (S : ℝ → ℂ) (h : ℝ) :
66     mellinIntegral S h = PaperX.RealAxisEndpointIntegral.endpointIntegral
67       (volume.restrict (Ioi 1)) (fun x : ℝ => (x ^ (-2 : ℝ)) • S x) Real.log h := by
68   unfold mellinIntegral PaperX.RealAxisEndpointIntegral.endpointIntegral
69   rw [← integral_smul]
70   apply integral_congr_ae
71   filter_upwards [ae_restrict_mem measurableSet_Ioi] with x hx
72   have hx0 : 0 < x := lt_trans zero_lt_one hx
73   rw [smul_smul, smul_smul]
74   congr 1
75   rw [Real.rpow_def_of_pos hx0, Real.rpow_def_of_pos hx0, mul_assoc, ← Real.exp_add]
76   congr 2
77   ring
78 
79 /-- A power-saving summatory bound gives a first-order right endpoint error
80 for its actual Mellin integral. -/
81 theorem mellinIntegral_sub_isBigO_of_power_bound {S : ℝ → ℂ} {C r : ℝ}
82     (hS : AEStronglyMeasurable S (volume.restrict (Ioi 1)))
83     (hr : r < 1)
84     (hbound : ∀ x, 1 < x → ‖S x‖ ≤ C * x ^ r) :
85     (fun h => mellinIntegral S h - mellinIntegral S 0)
86       =O[𝓝[>] (0 : ℝ)] (fun h : ℝ => h) := by
87   have hA : AEStronglyMeasurable (fun x : ℝ => (x ^ (-2 : ℝ)) • S x)
88       (volume.restrict (Ioi 1)) := by
89     have hm : Measurable (fun x : ℝ => x ^ (-2 : ℝ)) := by fun_prop
90     exact hm.aestronglyMeasurable.smul hS
91   have hu : ∀ᵐ x ∂volume.restrict (Ioi (1 : ℝ)), 0 ≤ Real.log x := by
92     filter_upwards [ae_restrict_mem measurableSet_Ioi] with x hx
93     exact Real.log_nonneg (le_of_lt hx)
94   have hW := integrable_weighted_moment_of_power_bound hS hr hbound
95   simpa only [mellinIntegral_eq_endpointIntegral] using
96     PaperX.RealAxisEndpointIntegral.endpointIntegral_sub_isBigO
97       (volume.restrict (Ioi 1)) hA Real.measurable_log hu hW
98 
99 end PaperX.RealAxisMellinMoment

Back to source controls