Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.kadiri_laplace_neg_line_weight_isBigO_atTop

PrimeNumberTheoremAnd.IEANTN.KadiriSupport · PrimeNumberTheoremAnd/IEANTN/KadiriSupport.lean:114 to 138

Source documentation

On atTop, the weighted source is O(exp (-(1 + b + σ) x)); no constraint on σ.

Exact Lean statement

lemma kadiri_laplace_neg_line_weight_isBigO_atTop {ψ : ℝ → ℂ} {b : ℝ} (sigma : ℝ)
    (hψ_decay : (fun x : ℝ ↦ ψ x * exp ((x : ℂ) / 2))
        =O[Filter.atTop] fun x : ℝ ↦ Real.exp (-(1/2 + b) * |x|)) :
    (fun x : ℝ => exp (-((sigma : ℂ) * (x : ℂ))) * ψ x)
      =O[Filter.atTop] fun x : ℝ => Real.exp (-(1 + b + sigma) * x)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma kadiri_laplace_neg_line_weight_isBigO_atTop {ψ : ℝ → ℂ} {b : ℝ} (sigma : ℝ)    (hψ_decay : (fun x : ℝ ↦ ψ x * exp ((x : ℂ) / 2))        =O[Filter.atTop] fun x : ℝ ↦ Real.exp (-(1/2 + b) * |x|)) :    (fun x : ℝ => exp (-((sigma : ℂ) * (x : ℂ))) * ψ x)      =O[Filter.atTop] fun x : ℝ => Real.exp (-(1 + b + sigma) * x) := by  rw [Asymptotics.isBigO_iff] at hψ_decay ⊢  obtain ⟨C, hC⟩ := hψ_decay  refine ⟨C, ?_⟩  filter_upwards [hC, Filter.eventually_gt_atTop (0 : ℝ)] with x hxC hxpos  rw [kadiri_laplace_neg_line_weight_norm_eq]  calc    Real.exp (-(sigma + 1 / 2) * x) * ‖ψ x * exp ((x : ℂ) / 2)‖        ≤ Real.exp (-(sigma + 1 / 2) * x) *            (C * ‖Real.exp (-(1 / 2 + b) * |x|)‖) := by          exact mul_le_mul_of_nonneg_left hxC (Real.exp_nonneg _)    _ = C * ‖Real.exp (-(1 + b + sigma) * x)‖ := by          rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_of_pos (Real.exp_pos _),            abs_of_pos (Real.exp_pos _), abs_of_pos hxpos]          calc            Real.exp (-(sigma + 1 / 2) * x) * (C * Real.exp (-(1 / 2 + b) * x))                = C * (Real.exp (-(sigma + 1 / 2) * x) *                    Real.exp (-(1 / 2 + b) * x)) := by ring_nf            _ = C * Real.exp (-(sigma + 1 / 2) * x + (-(1 / 2 + b) * x)) := by                  rw [Real.exp_add]            _ = C * Real.exp (-(1 + b + sigma) * x) := by ring_nf