RealAxisEndpointIntegral.lean

1 import Mathlib.MeasureTheory.Integral.Bochner.Basic
2 import Mathlib.Analysis.SpecialFunctions.Exp
3 import Mathlib.Analysis.Asymptotics.Defs
4 import Mathlib.Tactic
5 
6 /-! A logarithmic first moment gives a quantitative right endpoint bound for
7 an actual exponentially damped integral. Arithmetic character sums are not supplied
8 by this theorem. -/
9 
10 set_option autoImplicit false
11 noncomputable section
12 namespace PaperX.RealAxisEndpointIntegral
13 open MeasureTheory Filter
14 open scoped Topology
15 
16 /-- The elementary damping error, including the prefactor from partial summation. -/
17 theorem kernel_sub_one_le {h u : ℝ} (hh : 0 ≤ h) (hu : 0 ≤ u) :
18     |(1 + h) * Real.exp (-h * u) - 1| ≤ h * (1 + u) := by
19   have he0 : 0 ≤ Real.exp (-h * u) := (Real.exp_pos _).le
20   have he1 : Real.exp (-h * u) ≤ 1 := Real.exp_le_one_iff.mpr (by nlinarith)
21   have he2 := Real.add_one_le_exp (-h * u)
22   apply abs_le.mpr
23   constructor <;> nlinarith
24 
25 variable {α : Type*} [MeasurableSpace α] (μ : Measure α)
26 
27 /-- The actual integral that appears after writing x^(-h) as exp(-h log x). -/
28 def endpointIntegral (A : α → ℂ) (u : α → ℝ) (h : ℝ) : ℂ :=
29   ∫ x, ((1 + h) * Real.exp (-h * u x)) • A x ∂μ
30 
31 /-- At the endpoint the damping factor is exactly one. -/
32 theorem endpointIntegral_zero (A : α → ℂ) (u : α → ℝ) :
33     endpointIntegral μ A u 0 = ∫ x, A x ∂μ := by
34   simp [endpointIntegral]
35 
36 /-- The weighted first moment already implies integrability of the base function. -/
37 theorem integrable_of_weighted_moment {A : α → ℂ} {u : α → ℝ}
38     (hA : AEStronglyMeasurable A μ) (hu : ∀ᵐ x ∂μ, 0 ≤ u x)
39     (hW : Integrable (fun x => (1 + u x) * ‖A x‖) μ) : Integrable A μ := by
40   apply hW.mono' hA
41   filter_upwards [hu] with x hx
42   nlinarith [norm_nonneg (A x)]
43 
44 /-- Every nonnegative damping parameter gives an integrable kernel. -/
45 theorem integrable_kernel {A : α → ℂ} {u : α → ℝ}
46     (hA : AEStronglyMeasurable A μ) (humeas : Measurable u)
47     (hu : ∀ᵐ x ∂μ, 0 ≤ u x)
48     (hW : Integrable (fun x => (1 + u x) * ‖A x‖) μ)
49     {h : ℝ} (hh : 0 ≤ h) :
50     Integrable (fun x => ((1 + h) * Real.exp (-h * u x)) • A x) μ := by
51   have hAi := integrable_of_weighted_moment μ hA hu hW
52   apply (hAi.norm.const_mul (1 + h)).mono'
53   · exact ((measurable_const.mul ((measurable_const.mul humeas).exp)).aestronglyMeasurable).smul hA
54   · filter_upwards [hu] with x hx
55     rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg (by positivity)]
56     have he : Real.exp (-h * u x) ≤ 1 := Real.exp_le_one_iff.mpr (by nlinarith)
57     simpa only [mul_one] using mul_le_mul_of_nonneg_right
58       (mul_le_mul_of_nonneg_left he (by linarith : 0 ≤ 1 + h)) (norm_nonneg (A x))
59 
60 /-- A single finite weighted integral controls the right endpoint error linearly. -/
61 theorem endpointIntegral_sub_norm_le {A : α → ℂ} {u : α → ℝ}
62     (hA : AEStronglyMeasurable A μ) (humeas : Measurable u)
63     (hu : ∀ᵐ x ∂μ, 0 ≤ u x)
64     (hW : Integrable (fun x => (1 + u x) * ‖A x‖) μ)
65     {h : ℝ} (hh : 0 ≤ h) :
66     ‖endpointIntegral μ A u h - endpointIntegral μ A u 0‖ ≤
67       h * ∫ x, (1 + u x) * ‖A x‖ ∂μ := by
68   have hAi := integrable_of_weighted_moment μ hA hu hW
69   have hKi := integrable_kernel μ hA humeas hu hW hh
70   rw [endpointIntegral_zero, endpointIntegral, ← integral_sub hKi hAi]
71   calc
72     ‖∫ x, ((1 + h) * Real.exp (-h * u x)) • A x - A x ∂μ‖ ≤
73         ∫ x, ‖((1 + h) * Real.exp (-h * u x)) • A x - A x‖ ∂μ :=
74       norm_integral_le_integral_norm _
75     _ ≤ ∫ x, h * ((1 + u x) * ‖A x‖) ∂μ := by
76       apply integral_mono_ae (hKi.sub hAi).norm (hW.const_mul h)
77       filter_upwards [hu] with x hx
78       have he := kernel_sub_one_le hh hx
79       change ‖((1 + h) * Real.exp (-h * u x)) • A x - A x‖ ≤ _
80       have hid : ((1 + h) * Real.exp (-h * u x)) • A x - A x =
81           ((1 + h) * Real.exp (-h * u x) - 1) • A x := by rw [sub_smul, one_smul]
82       rw [hid, norm_smul, Real.norm_eq_abs]
83       exact (mul_le_mul_of_nonneg_right he (norm_nonneg (A x))).trans_eq (by ring)
84     _ = h * ∫ x, (1 + u x) * ‖A x‖ ∂μ := integral_const_mul _ _
85 
86 /-- The endpoint difference is O(h) along positive h tending to zero. -/
87 theorem endpointIntegral_sub_isBigO {A : α → ℂ} {u : α → ℝ}
88     (hA : AEStronglyMeasurable A μ) (humeas : Measurable u)
89     (hu : ∀ᵐ x ∂μ, 0 ≤ u x)
90     (hW : Integrable (fun x => (1 + u x) * ‖A x‖) μ) :
91     (fun h => endpointIntegral μ A u h - endpointIntegral μ A u 0)
92       =O[𝓝[>] (0 : ℝ)] (fun h : ℝ => h) := by
93   refine Asymptotics.isBigO_iff.mpr ⟨∫ x, (1 + u x) * ‖A x‖ ∂μ, ?_⟩
94   filter_upwards [self_mem_nhdsWithin] with h hh
95   have hh0 : 0 ≤ h := le_of_lt hh
96   simpa only [Real.norm_eq_abs, abs_of_nonneg hh0, mul_comm] using
97     endpointIntegral_sub_norm_le μ hA humeas hu hW hh0
98 
99 end PaperX.RealAxisEndpointIntegral

Back to source controls