Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.kadiri_thm_3_1_q1_eq_11_summed_pv_of_pointwise_inversion_bound

PrimeNumberTheoremAnd.IEANTN.KadiriEq11Reduction · PrimeNumberTheoremAnd/IEANTN/KadiriEq11Reduction.lean:454 to 499

Source documentation

Tannery exchange for the principal-value inversion terms. This converts pointwise PV inversion at each integer into the summed PV limit, using an explicit summable domination bound over n.

Exact Lean statement

lemma kadiri_thm_3_1_q1_eq_11_summed_pv_of_pointwise_inversion_bound
    {φ : ℝ → ℂ} {a : ℝ}
    (hinv : ∀ n : Nat, 1 ≤ n →
      let Φ : ℂ → ℂ := fun s ↦ ∫ y, φ y * exp (-s * (y : ℂ)) ∂volume
      Tendsto
        (fun T : ℝ =>
          (1 / (2 * (Real.pi : ℂ))) *
            ∫ t in (-T)..T,
              Φ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I) *
                (n : ℂ) ^ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I))
        atTop (𝓝 (φ (Real.log n))))
    {bound : ℕ → ℝ} (hbound_sum : Summable bound)
    (hbound :
      ∀ᶠ T in atTop, ∀ n : ℕ,
        ‖(Λ n : ℂ) *
          ((1 / (2 * (Real.pi : ℂ))) *
            ∫ t in (-T)..T,
              (let Φ : ℂ → ℂ := fun s ↦ ∫ y, φ y * exp (-s * (y : ℂ)) ∂volume
               Φ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I) *
                (n : ℂ) ^ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I)))‖ ≤ bound n) :
    Tendsto
      (fun T : ℝ =>
        ∑' n : ℕ,
          (Λ n : ℂ) *
            ((1 / (2 * (Real.pi : ℂ))) *
              ∫ t in (-T)..T,
                (let Φ : ℂ → ℂ := fun s ↦ ∫ y, φ y * exp (-s * (y : ℂ)) ∂volume
                 Φ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I) *
                  (n : ℂ) ^ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I))))
      atTop
      (𝓝 (∑' n : ℕ, (Λ n : ℂ) * φ (Real.log n)))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma kadiri_thm_3_1_q1_eq_11_summed_pv_of_pointwise_inversion_bound    {φ : ℝ → ℂ} {a : ℝ}    (hinv : ∀ n : Nat, 1 ≤ n →      let Φ : ℂ → ℂ := fun s ↦ ∫ y, φ y * exp (-s * (y : ℂ)) ∂volume      Tendsto        (fun T : ℝ =>          (1 / (2 * (Real.pi : ℂ))) *            ∫ t in (-T)..T,              Φ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I) *                (n : ℂ) ^ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I))        atTop (𝓝 (φ (Real.log n))))    {bound : ℕ → ℝ} (hbound_sum : Summable bound)    (hbound :      ∀ᶠ T in atTop, ∀ n : ℕ,        ‖(Λ n : ℂ) *          ((1 / (2 * (Real.pi : ℂ))) *            ∫ t in (-T)..T,              (let Φ : ℂ → ℂ := fun s ↦ ∫ y, φ y * exp (-s * (y : ℂ)) ∂volume               Φ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I) *                (n : ℂ) ^ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I)))‖ ≤ bound n) :    Tendsto      (fun T : ℝ =>        ∑' n : ℕ,          (Λ n : ℂ) *            ((1 / (2 * (Real.pi : ℂ))) *              ∫ t in (-T)..T,                (let Φ : ℂ → ℂ := fun s ↦ ∫ y, φ y * exp (-s * (y : ℂ)) ∂volume                 Φ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I) *                  (n : ℂ) ^ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I))))      atTop      (𝓝 (∑' n : ℕ, (Λ n : ℂ) * φ (Real.log n))) := by  refine tendsto_tsum_of_dominated_convergence    (𝓕 := atTop)    (f := fun T n =>      (Λ n : ℂ) *        ((1 / (2 * (Real.pi : ℂ))) *          ∫ t in (-T)..T,            (let Φ : ℂ → ℂ := fun s ↦ ∫ y, φ y * exp (-s * (y : ℂ)) ∂volume             Φ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I) *              (n : ℂ) ^ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I))))    (g := fun n => (Λ n : ℂ) * φ (Real.log n))    hbound_sum ?_ hbound  intro n  rcases Nat.eq_zero_or_pos n with rfl | hn  · simp  · simpa using (hinv n hn).const_mul (Λ n : ℂ)