Source indexedtheorem · leanprover/lean4:v4.32.0

Kadiri.kadiri_thm_3_1_q1_eq_11_of_inversion

PrimeNumberTheoremAnd.IEANTN.KadiriEq11Reduction · PrimeNumberTheoremAnd/IEANTN/KadiriEq11Reduction.lean:715 to 800

Source documentation

Reduction of Kadiri equation (11) from the pointwise inversion identity.

The analytic exchange of the von Mangoldt sum with the Mellin integral is kept as an explicit hypothesis. This isolates the part blocked by the concrete Fubini/Tonelli side-condition proof while avoiding any dependency on the sorried inversion theorem in Kadiri.lean.

Exact Lean statement

theorem kadiri_thm_3_1_q1_eq_11_of_inversion {φ : ℝ → ℂ} (_hφ : ContDiff ℝ 1 φ)
    {b : ℝ} (_hb : 0 < 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|))
    {a : ℝ} (ha : 0 < a) (_hab : a < b) (_ha1 : a < 1)
    (hinv : ∀ n : Nat, 1 ≤ n →
      let Φ : ℂ → ℂ := fun s ↦ ∫ y, φ y * exp (-s * (y : ℂ)) ∂volume
      (φ (Real.log n) : ℂ) =
        (1 / (2 * (Real.pi : ℂ))) *
          ∫ t : ℝ,
            Φ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I) *
              (n : ℂ) ^ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I))
    (hMellinSwap :
      let Φ : ℂ → ℂ := fun s ↦ ∫ y, φ y * exp (-s * (y : ℂ)) ∂volume
      (∑' n : ℕ,
          (Λ n : ℂ) *
            ((1 / (2 * (Real.pi : ℂ))) *
              ∫ t : ℝ,
                Φ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I) *
                  (n : ℂ) ^ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I))) =
        (1 / (2 * (Real.pi : ℂ))) *
          ∫ t : ℝ,
            (∑' n : ℕ,
                (Λ n : ℂ) *
                  (n : ℂ) ^ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I)) *
              Φ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I)) :
    let Φ : ℂ → ℂ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem kadiri_thm_3_1_q1_eq_11_of_inversion {φ : ℝ → ℂ} (_hφ : ContDiff ℝ 1 φ)    {b : ℝ} (_hb : 0 < 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|))    {a : ℝ} (ha : 0 < a) (_hab : a < b) (_ha1 : a < 1)    (hinv : ∀ n : Nat, 1 ≤ n →      let Φ : ℂ → ℂ := fun s ↦ ∫ y, φ y * exp (-s * (y : ℂ)) ∂volume      (φ (Real.log n) : ℂ) =        (1 / (2 * (Real.pi : ℂ))) *          ∫ t : ℝ,            Φ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I) *              (n : ℂ) ^ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I))    (hMellinSwap :      let Φ : ℂ → ℂ := fun s ↦ ∫ y, φ y * exp (-s * (y : ℂ)) ∂volume      (∑' n : ℕ,          (Λ n : ℂ) *            ((1 / (2 * (Real.pi : ℂ))) *              ∫ t : ℝ,                Φ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I) *                  (n : ℂ) ^ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I))) =        (1 / (2 * (Real.pi : ℂ))) *          ∫ t : ℝ,            (∑' n : ℕ,                (Λ n : ℂ) *                  (n : ℂ) ^ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I)) *              Φ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I)) :    let Φ : ℂ → ℂ := fun s ↦ ∫ y, φ y * exp (-s * (y : ℂ)) ∂volume    (∑' n : ℕ, (Λ n : ℂ) * φ (Real.log n)) =      (1 / (2 * (Real.pi : ℂ))) *        ∫ t : ℝ,          (-deriv riemannZeta (((1 + a : ℝ) : ℂ) + (t : ℂ) * I) /              riemannZeta (((1 + a : ℝ) : ℂ) + (t : ℂ) * I)) *            Φ (-(((1 + a : ℝ) : ℂ) + (t : ℂ) * I)) := by  intro Φ  dsimp only at hMellinSwap  have hterm :      ∀ n : ℕ,        (Λ n : ℂ) * φ (Real.log n) =          (Λ n : ℂ) *            ((1 / (2 * (Real.pi : ℂ))) *              ∫ t : ℝ,                Φ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I) *                  (n : ℂ) ^ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I)) := by    intro n    rcases Nat.eq_zero_or_pos n with rfl | hn    · simp    · rw [hinv n hn]  rw [tsum_congr hterm]  rw [hMellinSwap]  have hcollapse :      (∫ t : ℝ,          (∑' n : ℕ,              (Λ n : ℂ) *                (n : ℂ) ^ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I)) *            Φ ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I)) =        ∫ t : ℝ,          (-deriv riemannZeta (((1 + a : ℝ) : ℂ) + (t : ℂ) * I) /              riemannZeta (((1 + a : ℝ) : ℂ) + (t : ℂ) * I)) *            Φ (-(((1 + a : ℝ) : ℂ) + (t : ℂ) * I)) := by    let F : ℝ → ℂ := fun t ↦      (-deriv riemannZeta (((1 + a : ℝ) : ℂ) + (t : ℂ) * I) /          riemannZeta (((1 + a : ℝ) : ℂ) + (t : ℂ) * I)) *        Φ (-(((1 + a : ℝ) : ℂ) + (t : ℂ) * I))    have hneg : (∫ t : ℝ, F (-t)) = ∫ t : ℝ, F t := by      simpa using        (Measure.measurePreserving_neg (volume : Measure ℝ)).integral_comp          (Homeomorph.neg ℝ).measurableEmbedding F    rw [← hneg]    refine integral_congr_ae ?_    filter_upwards with t    dsimp [F]    rw [tsum_vonMangoldt_neg_mellin_line ha t]    have hzeta_arg :        (((1 + a : ℝ) : ℂ) - (t : ℂ) * I) =          (((1 + a : ℝ) : ℂ) + ((-t : ℝ) : ℂ) * I) := by      simp only [ofReal_neg]      ring    have hPhi_arg :        ((-(1 + a : ℝ) : ℂ) + (t : ℂ) * I) =          -(((1 + a : ℝ) : ℂ) + ((-t : ℝ) : ℂ) * I) := by      simp only [ofReal_neg]      ring    rw [hzeta_arg, hPhi_arg]  rw [hcollapse]