Source indexedlemma · leanprover/lean4:v4.32.0

RectangleIntegral_tendsTo_VerticalIntegral

PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:38 to 65

Source documentation

Obvious. -/) (latexEnv := "lemma")] lemma zeroTendstoDiff (L₁ L₂ : ℂ) (f : ℝ → ℂ) (h : ∀ᶠ T in atTop, f T = 0) (h' : Tendsto f atTop (𝓝 (L₂ - L₁))) : L₁ = L₂ := by rw [← zero_add L₁, ← @eq_sub_iff_add_eq] exact tendsto_nhds_unique (EventuallyEq.tendsto h) h'

/- TODO: Move this to general section.

Exact Lean statement

@[blueprint
  (title := "RectangleIntegral-tendsTo-VerticalIntegral")
  (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 \pm \infty$.
  Then the limit of rectangle integrals
  $$\lim_{T\to\infty}\int_{\sigma-iT}^{\sigma'+iT}f(s)ds =
  \int_{(\sigma')}f(s)ds - \int_{(\sigma)}f(s)ds.$$
  -/)
  (proof := /-- Almost by definition. -/)
  (proofUses := ["RectangleIntegral"])
  (latexEnv := "lemma")]
lemma RectangleIntegral_tendsTo_VerticalIntegral {σ σ' : ℝ} {f : ℂ → ℂ}
    (hbot : Tendsto (fun (y : ℝ) ↦ ∫ (x : ℝ) in σ..σ', f (x + y * I)) atBot (𝓝 0))
    (htop : Tendsto (fun (y : ℝ) ↦ ∫ (x : ℝ) in σ..σ', f (x + y * I)) atTop (𝓝 0))
    (hleft : Integrable (fun (y : ℝ) ↦ f (σ + y * I)))
    (hright : Integrable (fun (y : ℝ) ↦ f (σ' + y * I))) :
    Tendsto (fun (T : ℝ) ↦ RectangleIntegral f (σ - I * T) (σ' + I * T)) atTop
      (𝓝 (VerticalIntegral f σ' - VerticalIntegral f σ))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  (title := "RectangleIntegral-tendsTo-VerticalIntegral")  (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 \pm \infty$.  Then the limit of rectangle integrals  $$\lim_{T\to\infty}\int_{\sigma-iT}^{\sigma'+iT}f(s)ds =  \int_{(\sigma')}f(s)ds - \int_{(\sigma)}f(s)ds.$$  -/)  (proof := /-- Almost by definition. -/)  (proofUses := ["RectangleIntegral"])  (latexEnv := "lemma")]lemma RectangleIntegral_tendsTo_VerticalIntegral {σ σ' : ℝ} {f : ℂ → ℂ}    (hbot : Tendsto (fun (y : ℝ) ↦ ∫ (x : ℝ) in σ..σ', f (x + y * I)) atBot (𝓝 0))    (htop : Tendsto (fun (y : ℝ) ↦ ∫ (x : ℝ) in σ..σ', f (x + y * I)) atTop (𝓝 0))    (hleft : Integrable (fun (y : ℝ) ↦ f (σ + y * I)))    (hright : Integrable (fun (y : ℝ) ↦ f (σ' + y * I))) :    Tendsto (fun (T : ℝ) ↦ RectangleIntegral f (σ - I * T) (σ' + I * T)) atTop      (𝓝 (VerticalIntegral f σ' - VerticalIntegral f σ)) := by  simp only [RectangleIntegral, sub_re, ofReal_re, mul_re, I_re, zero_mul, I_im, ofReal_im,    mul_zero, sub_self, sub_zero, add_re, add_zero, sub_im, mul_im, one_mul, zero_add, zero_sub,    add_im]  apply Tendsto.sub  · rewrite [← zero_add (VerticalIntegral _ _), ← zero_sub_zero]    apply Tendsto.add <| Tendsto.sub (hbot.comp tendsto_neg_atTop_atBot) htop    exact (intervalIntegral_tendsto_integral hright tendsto_neg_atTop_atBot tendsto_id).const_smul I  · exact (intervalIntegral_tendsto_integral hleft tendsto_neg_atTop_atBot tendsto_id).const_smul I