Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.kadiri_laplace_neg_line_weight_deriv_bounded

PrimeNumberTheoremAnd.IEANTN.KadiriSupport · PrimeNumberTheoremAnd/IEANTN/KadiriSupport.lean:185 to 213

Source documentation

Global bound for the derivative of the weighted source for -(1+b) < σ < b.

Exact Lean statement

lemma kadiri_laplace_neg_line_weight_deriv_bounded {φ : ℝ → ℂ} (hφ : ContDiff ℝ 1 φ)
    {b sigma : ℝ} (hlo : -(1 + b) < sigma) (hhi : sigma < b)
    (hφ_decay : (fun x : ℝ ↦ φ x * exp ((x : ℂ) / 2))
        =O[Filter.cocompact ℝ] fun x : ℝ ↦ Real.exp (-(1/2 + b) * |x|))
    (hφ'_decay : (fun x : ℝ ↦ deriv φ x * exp ((x : ℂ) / 2))
        =O[Filter.cocompact ℝ] fun x : ℝ ↦ Real.exp (-(1/2 + b) * |x|)) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ y : ℝ,
      ‖deriv (fun x : ℝ => exp (-((sigma : ℂ) * (x : ℂ))) * φ x) y‖ ≤ D

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma kadiri_laplace_neg_line_weight_deriv_bounded {φ : ℝ → ℂ} (hφ : ContDiff ℝ 1 φ)    {b sigma : ℝ} (hlo : -(1 + b) < sigma) (hhi : sigma < b)    (hφ_decay : (fun x : ℝ ↦ φ x * exp ((x : ℂ) / 2))        =O[Filter.cocompact ℝ] fun x : ℝ ↦ Real.exp (-(1/2 + b) * |x|))    (hφ'_decay : (fun x : ℝ ↦ deriv φ x * exp ((x : ℂ) / 2))        =O[Filter.cocompact ℝ] fun x : ℝ ↦ Real.exp (-(1/2 + b) * |x|)) :    ∃ D : ℝ, 0 ≤ D ∧ ∀ y : ℝ,      ‖deriv (fun x : ℝ => exp (-((sigma : ℂ) * (x : ℂ))) * φ x) y‖ ≤ D := by  obtain ⟨Bφ, hBφ_nonneg, hBφ⟩ :=    kadiri_laplace_neg_line_weight_bounded_of_continuous hφ.continuous hlo hhi hφ_decay  obtain ⟨Bφ', hBφ'_nonneg, hBφ'⟩ :=    kadiri_laplace_neg_line_weight_bounded_of_continuous      (hφ.continuous_deriv (by norm_num)) hlo hhi hφ'_decay  refine ⟨‖(sigma : ℂ)‖ * Bφ + Bφ',    add_nonneg (mul_nonneg (norm_nonneg _) hBφ_nonneg) hBφ'_nonneg, ?_⟩  intro y  rw [kadiri_laplace_neg_line_weight_deriv hφ sigma y]  calc    ‖-(sigma : ℂ) * (exp (-((sigma : ℂ) * (y : ℂ))) * φ y) +        exp (-((sigma : ℂ) * (y : ℂ))) * deriv φ y‖        ≤ ‖-(sigma : ℂ) * (exp (-((sigma : ℂ) * (y : ℂ))) * φ y)‖ +            ‖exp (-((sigma : ℂ) * (y : ℂ))) * deriv φ y‖ := norm_add_le _ _    _ ≤ ‖(sigma : ℂ)‖ * Bφ + Bφ' := by          have hfirst :              ‖-(sigma : ℂ) * (exp (-((sigma : ℂ) * (y : ℂ))) * φ y)‖ ≤                ‖(sigma : ℂ)‖ * Bφ := by            rw [norm_mul, norm_neg]            exact mul_le_mul_of_nonneg_left (hBφ y) (norm_nonneg _)          exact add_le_add hfirst (hBφ' y)