Source indexedlemma · leanprover/lean4:v4.32.0

RectangleIntegral_tendsTo_LowerU

PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:240 to 287

Mathematical statement

Exact Lean statement

@[blueprint
  (title := "RectangleIntegral-tendsTo-LowerU")
  (statement := /--
  Let $\sigma,\sigma' \in \mathbb{R}$, and $f : \mathbb{C} \to \mathbb{C}$ such that
  the vertical integrals $\int_{(\sigma)}f(s)ds$ and $\int_{(\sigma')}f(s)ds$ exist and
  the horizontal integral $\int_{(\sigma)}^{\sigma'}f(x + yi)dx$ vanishes as $y \to -\infty$.
  Then the limit of rectangle integrals
  $$\int_{\sigma-iU}^{\sigma'-iT}f(s)ds$$
  as $U\to\infty$ is the ``LowerUIntegral'' of $f$.
  -/)
  (proof := /-- Almost by definition. -/)
  (proofUses := ["RectangleIntegral", "LowerUIntegral"])
  (latexEnv := "lemma")]
lemma RectangleIntegral_tendsTo_LowerU {σ σ' T : ℝ} {f : ℂ → ℂ}
    (hbot : Tendsto (fun (y : ℝ) ↦ ∫ (x : ℝ) in σ..σ', f (x + y * I)) atBot (𝓝 0))
    (hleft : Integrable (fun (y : ℝ) ↦ f (σ + y * I)))
    (hright : Integrable (fun (y : ℝ) ↦ f (σ' + y * I))) :
    Tendsto (fun (U : ℝ) ↦ RectangleIntegral f (σ - I * U) (σ' - I * T)) atTop
      (𝓝 (- LowerUIntegral f σ σ' T))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  (title := "RectangleIntegral-tendsTo-LowerU")  (statement := /--  Let $\sigma,\sigma' \in \mathbb{R}$, and $f : \mathbb{C} \to \mathbb{C}$ such that  the vertical integrals $\int_{(\sigma)}f(s)ds$ and $\int_{(\sigma')}f(s)ds$ exist and  the horizontal integral $\int_{(\sigma)}^{\sigma'}f(x + yi)dx$ vanishes as $y \to -\infty$.  Then the limit of rectangle integrals  $$\int_{\sigma-iU}^{\sigma'-iT}f(s)ds$$  as $U\to\infty$ is the ``LowerUIntegral'' of $f$.  -/)  (proof := /-- Almost by definition. -/)  (proofUses := ["RectangleIntegral", "LowerUIntegral"])  (latexEnv := "lemma")]lemma RectangleIntegral_tendsTo_LowerU {σ σ' T : ℝ} {f : ℂ → ℂ}    (hbot : Tendsto (fun (y : ℝ) ↦ ∫ (x : ℝ) in σ..σ', f (x + y * I)) atBot (𝓝 0))    (hleft : Integrable (fun (y : ℝ) ↦ f (σ + y * I)))    (hright : Integrable (fun (y : ℝ) ↦ f (σ' + y * I))) :    Tendsto (fun (U : ℝ) ↦ RectangleIntegral f (σ - I * U) (σ' - I * T)) atTop      (𝓝 (- LowerUIntegral f σ σ' T)) := by  have h_re  (s : ℝ) (t : ℝ) : (s  - I * t).re = s  := by simp  have h_im  (s : ℝ) (t : ℝ) : (s  - I * t).im = -t  := by simp  have hbot' :      Tendsto (fun (y : ℝ) ↦ ∫ (x : ℝ) in σ..σ', f (x - y * I)) atTop (𝓝 0) := by    convert (hbot.comp tendsto_neg_atTop_atBot) using 1    ext; simp only [Function.comp_apply, ofReal_neg, neg_mul]; rfl  have htop : Tendsto (fun (_ : ℝ) ↦ ∫ (x : ℝ) in σ..σ', f (x - T * I)) atTop      (𝓝 <| ∫ (x : ℝ) in σ..σ', f (x - T * I)) := tendsto_const_nhds  have hvert (s : ℝ) (int : Integrable (fun (y : ℝ) ↦ f (s + y * I))) :      Tendsto (fun (U : ℝ) ↦ I * ∫ (y : ℝ) in -U..-T, f (s + y * I)) atTop        (𝓝 <| I * ∫ (y : ℝ) in Iic (-T), f (s + y * I)) := by    have := (intervalIntegral_tendsto_integral_Iic (-T) int.restrict tendsto_id).const_smul I    convert! (this.comp tendsto_neg_atTop_atBot) using 1  have := ((hbot'.sub htop).add (hvert σ' hright)).sub (hvert σ hleft)  rw [zero_sub] at this  simp_rw [RectangleIntegral, LowerUIntegral, HIntegral, VIntegral, h_re, h_im, ofReal_neg, neg_mul,    neg_add_rev, neg_sub]  have final :      (((-∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I)) +          I * ∫ (y : ℝ) in Iic (-T), f (↑σ' + ↑y * I)) -          I * ∫ (y : ℝ) in Iic (-T), f (↑σ + ↑y * I)) =      (-(I * ∫ (y : ℝ) in Iic (-T), f (↑σ + ↑y * I)) +        ((I * ∫ (y : ℝ) in Iic (-T), f (↑σ' + ↑y * I)) -          ∫ (x : ℝ) in σ..σ', f (↑x - ↑T * I))) := by    ring_nf    congr    ext    ring_nf  exact final ▸ this